T:Type, L:(T List), a,b:T. l_before(a; b; L; T)  (a  L) 

latex

Definitions	t  T, l_before(x; y; l; T), P  Q, x:A. B(x), P  Q, P  Q, P  Q, True, P  Q, prop{i:l}
Lemmas	sublist wf, member iff sublist, sublist transitivity, cons sublist cons, nil sublist, and functionality wrt iff, or functionality wrt iff, true wf